0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 23 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 2 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 UsableRulesReductionPairsProof (⇔, 127 ms)
↳20 QDP
↳21 MRRProof (⇔, 0 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(U, V, W, Z, append_in_gga(U, V, U1))
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → APPEND_IN_GGA(U, V, U1)
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → U1_GGA(U, V, Y, Z, append_in_gga(V, Y, Z))
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → APPEND_IN_GGA(V, Y, Z)
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → U3_GG(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → APPEND_IN_GGA(W, Z, W1)
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_GG(U, V, W, Z, lessleaves_in_gg(U1, W1))
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → LESSLEAVES_IN_GG(U1, W1)
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(U, V, W, Z, append_in_gga(U, V, U1))
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → APPEND_IN_GGA(U, V, U1)
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → U1_GGA(U, V, Y, Z, append_in_gga(V, Y, Z))
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → APPEND_IN_GGA(V, Y, Z)
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → U3_GG(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → APPEND_IN_GGA(W, Z, W1)
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_GG(U, V, W, Z, lessleaves_in_gg(U1, W1))
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → LESSLEAVES_IN_GG(U1, W1)
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → APPEND_IN_GGA(V, Y, Z)
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
APPEND_IN_GGA(cons(U, V), Y, cons(U, Z)) → APPEND_IN_GGA(V, Y, Z)
APPEND_IN_GGA(cons(U, V), Y) → APPEND_IN_GGA(V, Y)
From the DPs we obtained the following set of size-change graphs:
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → U3_GG(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → LESSLEAVES_IN_GG(U1, W1)
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(U, V, W, Z, append_in_gga(U, V, U1))
lessleaves_in_gg(nil, cons(W, Z)) → lessleaves_out_gg(nil, cons(W, Z))
lessleaves_in_gg(cons(U, V), cons(W, Z)) → U2_gg(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_gg(U, V, W, Z, append_out_gga(U, V, U1)) → U3_gg(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_gg(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → U4_gg(U, V, W, Z, lessleaves_in_gg(U1, W1))
U4_gg(U, V, W, Z, lessleaves_out_gg(U1, W1)) → lessleaves_out_gg(cons(U, V), cons(W, Z))
U2_GG(U, V, W, Z, append_out_gga(U, V, U1)) → U3_GG(U, V, W, Z, U1, append_in_gga(W, Z, W1))
U3_GG(U, V, W, Z, U1, append_out_gga(W, Z, W1)) → LESSLEAVES_IN_GG(U1, W1)
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(U, V, W, Z, append_in_gga(U, V, U1))
append_in_gga(nil, Y, Y) → append_out_gga(nil, Y, Y)
append_in_gga(cons(U, V), Y, cons(U, Z)) → U1_gga(U, V, Y, Z, append_in_gga(V, Y, Z))
U1_gga(U, V, Y, Z, append_out_gga(V, Y, Z)) → append_out_gga(cons(U, V), Y, cons(U, Z))
U2_GG(W, Z, append_out_gga(U1)) → U3_GG(U1, append_in_gga(W, Z))
U3_GG(U1, append_out_gga(W1)) → LESSLEAVES_IN_GG(U1, W1)
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(W, Z, append_in_gga(U, V))
append_in_gga(nil, Y) → append_out_gga(Y)
append_in_gga(cons(U, V), Y) → U1_gga(U, append_in_gga(V, Y))
U1_gga(U, append_out_gga(Z)) → append_out_gga(cons(U, Z))
append_in_gga(x0, x1)
U1_gga(x0, x1)
Used ordering: POLO with Polynomial interpretation [POLO]:
append_in_gga(nil, Y) → append_out_gga(Y)
POL(LESSLEAVES_IN_GG(x1, x2)) = 1 + x1 + x2
POL(U1_gga(x1, x2)) = 2·x1 + x2
POL(U2_GG(x1, x2, x3)) = 1 + 2·x1 + x2 + x3
POL(U3_GG(x1, x2)) = 1 + x1 + x2
POL(append_in_gga(x1, x2)) = x1 + x2
POL(append_out_gga(x1)) = x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(nil) = 2
U2_GG(W, Z, append_out_gga(U1)) → U3_GG(U1, append_in_gga(W, Z))
U3_GG(U1, append_out_gga(W1)) → LESSLEAVES_IN_GG(U1, W1)
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(W, Z, append_in_gga(U, V))
append_in_gga(cons(U, V), Y) → U1_gga(U, append_in_gga(V, Y))
U1_gga(U, append_out_gga(Z)) → append_out_gga(cons(U, Z))
append_in_gga(x0, x1)
U1_gga(x0, x1)
U2_GG(W, Z, append_out_gga(U1)) → U3_GG(U1, append_in_gga(W, Z))
U3_GG(U1, append_out_gga(W1)) → LESSLEAVES_IN_GG(U1, W1)
LESSLEAVES_IN_GG(cons(U, V), cons(W, Z)) → U2_GG(W, Z, append_in_gga(U, V))
append_in_gga(cons(U, V), Y) → U1_gga(U, append_in_gga(V, Y))
U1_gga(U, append_out_gga(Z)) → append_out_gga(cons(U, Z))
appendingga2 > cons2 > U2GG3 > U3GG2 > LESSLEAVESINGG2 > U1gga2 > appendoutgga1
append_out_gga_1=1
cons_2=0
U1_gga_2=0
U2_GG_3=0
U3_GG_2=1
append_in_gga_2=0
LESSLEAVES_IN_GG_2=2
append_in_gga(x0, x1)
U1_gga(x0, x1)